Nuprl Definition : p-filter 11,40

p-filter(f)(x) == case f(x) of inl(p) => inl x  | inr(p) => inr p  
latex


Definitionsx.A(x), case b of inl(x) => s(x) | inr(y) => t(y), f(a), inl x , inr x 
FDL editor aliasesp-filter

origin